Inference at * 1 2 
Iof proof for Lemma sub-equality:



1. T : Type
2. P : T
3. i : T
4. u : T
5. i = u
6. P(u)
7. P(i)
  i = u 

latex

 by EqTypeCD 

latex

 1: 

 1:   i = u
 2: .....set predicate..... NILNIL

 2:   {j:T| P(j)} 
 3: .....wf..... NILNIL

 3: 8. T
 3:   {j:T| P(j)}  = {j:T| P(j)} 
 .

Definitions

{x:A| B(x)} , f(a)